From febe38a27a9aaa0b31a6094d89f97a9c13628f39 Mon Sep 17 00:00:00 2001 From: Pawel Gebal Date: Wed, 8 May 2024 18:10:58 +0200 Subject: [PATCH] SMTChecker: add insufficient funds verification target for CHC engine --- Changelog.md | 2 +- libsolidity/formal/BMC.cpp | 6 +++ libsolidity/formal/CHC.cpp | 18 +++++++ .../model_checker_targets_all_all_engines/err | 14 +----- .../model_checker_targets_all_chc/err | 2 + .../model_checker_targets_balance_chc/err | 1 + .../err | 14 +----- .../model_checker_targets_default_chc/err | 2 + .../output.json | 12 +++++ .../output.json | 49 ++++--------------- .../output.json | 10 ++++ .../blockchain_state/balance_spend.sol | 3 +- .../blockchain_state/balance_spend_2.sol | 6 +-- .../blockchain_state/decreasing_balance.sol | 2 +- .../blockchain_state/free_function_2.sol | 3 +- .../blockchain_state/library_internal_2.sol | 3 +- .../blockchain_state/library_public_2.sol | 2 +- .../{transfer.sol => transfer_1.sol} | 3 +- .../blockchain_state/transfer_2.sol | 14 ++++++ .../blockchain_state/transfer_3.sol | 11 +++++ .../blockchain_state/transfer_4.sol | 12 +++++ .../smtCheckerTests/functions/this_state.sol | 14 +++--- .../types/address_transfer.sol | 2 +- .../types/address_transfer_2.sol | 4 +- .../types/address_transfer_3.sol | 3 +- .../types/address_transfer_insufficient.sol | 4 +- 26 files changed, 125 insertions(+), 91 deletions(-) create mode 100644 test/cmdlineTests/model_checker_targets_balance_chc/err rename test/libsolidity/smtCheckerTests/blockchain_state/{transfer.sol => transfer_1.sol} (66%) create mode 100644 test/libsolidity/smtCheckerTests/blockchain_state/transfer_2.sol create mode 100644 test/libsolidity/smtCheckerTests/blockchain_state/transfer_3.sol create mode 100644 test/libsolidity/smtCheckerTests/blockchain_state/transfer_4.sol diff --git a/Changelog.md b/Changelog.md index 252f228c5330..4ed7bd2a360c 100644 --- a/Changelog.md +++ b/Changelog.md @@ -5,7 +5,7 @@ Language Features: Compiler Features: - +* SMTChecker: Create balance check verification target for CHC engine. Bugfixes: * Commandline Interface: Fix ICE when the optimizer is disabled and an empty/blank string is used for ``--yul-optimizations`` sequence. diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 932a315a703a..97dd7050fef8 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -1050,6 +1050,12 @@ void BMC::checkDivByZero(BMCVerificationTarget& _target) void BMC::checkBalance(BMCVerificationTarget& _target) { solAssert(_target.type == VerificationTargetType::Balance, ""); + + if ( + m_solvedTargets.count(_target.expression) && + m_solvedTargets.at(_target.expression).count(VerificationTargetType::Balance) + ) + return; checkCondition( _target, _target.constraints && _target.value, diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 2c9075abcc4a..b6ffd5954ffb 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -607,6 +607,22 @@ void CHC::endVisit(FunctionCall const& _funCall) SMTEncoder::endVisit(_funCall); unknownFunctionCall(_funCall); break; + case FunctionType::Kind::Send: + case FunctionType::Kind::Transfer: + { + auto value = _funCall.arguments().front(); + solAssert(value, ""); + smtutil::Expression thisBalance = state().balance(); + + verificationTargetEncountered( + &_funCall, + VerificationTargetType::Balance, + thisBalance < expr(*value) + ); + + SMTEncoder::endVisit(_funCall); + break; + } case FunctionType::Kind::KECCAK256: case FunctionType::Kind::ECRecover: case FunctionType::Kind::SHA256: @@ -2013,6 +2029,8 @@ std::pair CHC::targetDescription(CHCVerificationTarget con return {"Division by zero", 4281_error}; else if (_target.type == VerificationTargetType::Assert) return {"Assertion violation", 6328_error}; + else if (_target.type == VerificationTargetType::Balance) + return {"Insufficient funds", 8656_error}; else solAssert(false); } diff --git a/test/cmdlineTests/model_checker_targets_all_all_engines/err b/test/cmdlineTests/model_checker_targets_all_all_engines/err index cc8a8ea33d1c..c67d97b61216 100644 --- a/test/cmdlineTests/model_checker_targets_all_all_engines/err +++ b/test/cmdlineTests/model_checker_targets_all_all_engines/err @@ -88,21 +88,11 @@ test.f(0x0, 1) 13 | arr[x]; | ^^^^^^ +Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. + Warning: BMC: Condition is always true. --> model_checker_targets_all_all_engines/input.sol:6:11: | 6 | require(x >= 0); | ^^^^^^ Note: Callstack: - -Warning: BMC: Insufficient funds happens here. - --> model_checker_targets_all_all_engines/input.sol:10:3: - | -10 | a.transfer(x); - | ^^^^^^^^^^^^^ -Note: Counterexample: - a = 0 - x = 0 - -Note: Callstack: -Note: diff --git a/test/cmdlineTests/model_checker_targets_all_chc/err b/test/cmdlineTests/model_checker_targets_all_chc/err index d0404ecfb6b9..9c257cefe9eb 100644 --- a/test/cmdlineTests/model_checker_targets_all_chc/err +++ b/test/cmdlineTests/model_checker_targets_all_chc/err @@ -87,3 +87,5 @@ test.f(0x0, 1) | 13 | arr[x]; | ^^^^^^ + +Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/cmdlineTests/model_checker_targets_balance_chc/err b/test/cmdlineTests/model_checker_targets_balance_chc/err new file mode 100644 index 000000000000..57bfe42678e4 --- /dev/null +++ b/test/cmdlineTests/model_checker_targets_balance_chc/err @@ -0,0 +1 @@ +Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/cmdlineTests/model_checker_targets_default_all_engines/err b/test/cmdlineTests/model_checker_targets_default_all_engines/err index c1fe2f5b3e59..62d3b203cb9c 100644 --- a/test/cmdlineTests/model_checker_targets_default_all_engines/err +++ b/test/cmdlineTests/model_checker_targets_default_all_engines/err @@ -58,21 +58,11 @@ test.f(0x0, 1) 13 | arr[x]; | ^^^^^^ +Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. + Warning: BMC: Condition is always true. --> model_checker_targets_default_all_engines/input.sol:6:11: | 6 | require(x >= 0); | ^^^^^^ Note: Callstack: - -Warning: BMC: Insufficient funds happens here. - --> model_checker_targets_default_all_engines/input.sol:10:3: - | -10 | a.transfer(x); - | ^^^^^^^^^^^^^ -Note: Counterexample: - a = 0 - x = 0 - -Note: Callstack: -Note: diff --git a/test/cmdlineTests/model_checker_targets_default_chc/err b/test/cmdlineTests/model_checker_targets_default_chc/err index bd2aa0b4de1d..70f3c5bc6072 100644 --- a/test/cmdlineTests/model_checker_targets_default_chc/err +++ b/test/cmdlineTests/model_checker_targets_default_chc/err @@ -57,3 +57,5 @@ test.f(0x0, 1) | 13 | arr[x]; | ^^^^^^ + +Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/cmdlineTests/standard_model_checker_targets_balance_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_balance_chc/output.json index f047ff70a9eb..9d3e40b708f1 100644 --- a/test/cmdlineTests/standard_model_checker_targets_balance_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_balance_chc/output.json @@ -1,4 +1,16 @@ { + "errors": [ + { + "component": "general", + "errorCode": "1391", + "formattedMessage": "Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them. + +", + "message": "CHC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them.", + "severity": "info", + "type": "Info" + } + ], "sources": { "A": { "id": 0 diff --git a/test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json b/test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json index 2318e5adfaba..8f20d854bfb5 100644 --- a/test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json @@ -148,6 +148,16 @@ test.f(0x0, 1)", }, "type": "Warning" }, + { + "component": "general", + "errorCode": "1391", + "formattedMessage": "Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them. + +", + "message": "CHC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them.", + "severity": "info", + "type": "Info" + }, { "component": "general", "errorCode": "6838", @@ -172,45 +182,6 @@ Note: Callstack: "start": 159 }, "type": "Warning" - }, - { - "component": "general", - "errorCode": "1236", - "formattedMessage": "Warning: BMC: Insufficient funds happens here. - --> A:11:7: - | -11 | \t\t\t\t\t\ta.transfer(x); - | \t\t\t\t\t\t^^^^^^^^^^^^^ -Note: Counterexample: - a = 0 - x = 0 - -Note: Callstack: -Note: - -", - "message": "BMC: Insufficient funds happens here.", - "secondarySourceLocations": [ - { - "message": "Counterexample: - a = 0 - x = 0 -" - }, - { - "message": "Callstack:" - }, - { - "message": "" - } - ], - "severity": "warning", - "sourceLocation": { - "end": 237, - "file": "A", - "start": 224 - }, - "type": "Warning" } ], "sources": { diff --git a/test/cmdlineTests/standard_model_checker_targets_default_chc/output.json b/test/cmdlineTests/standard_model_checker_targets_default_chc/output.json index eb39e0271233..e045a8bff49a 100644 --- a/test/cmdlineTests/standard_model_checker_targets_default_chc/output.json +++ b/test/cmdlineTests/standard_model_checker_targets_default_chc/output.json @@ -147,6 +147,16 @@ test.f(0x0, 1)", "start": 283 }, "type": "Warning" + }, + { + "component": "general", + "errorCode": "1391", + "formattedMessage": "Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them. + +", + "message": "CHC: 1 verification condition(s) proved safe! Enable the model checker option \"show proved safe\" to see all of them.", + "severity": "info", + "type": "Info" } ], "sources": { diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol index 387e45bb9f46..720ab5695029 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol @@ -19,5 +19,4 @@ contract C { // SMTIgnoreCex: yes // ---- // Warning 6328: (280-314): CHC: Assertion violation happens here. -// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. -// Warning 1236: (175-190): BMC: Insufficient funds happens here. +// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol index 5df0b99956f2..3ceac964f111 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol @@ -15,9 +15,9 @@ contract C { // ==== // SMTEngine: all // SMTIgnoreCex: yes +// SMTIgnoreOS: macos // ---- -// Warning 6328: (193-226): CHC: Assertion violation might happen here. +// Warning 8656: (141-156): CHC: Insufficient funds happens here. +// Warning 6328: (193-226): CHC: Assertion violation happens here. // Warning 6328: (245-279): CHC: Assertion violation happens here. // Warning 6328: (298-332): CHC: Assertion violation happens here. -// Warning 1236: (141-156): BMC: Insufficient funds happens here. -// Warning 4661: (193-226): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol b/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol index 76455060d8d5..df35a2785824 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol @@ -18,4 +18,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Info 6002: BMC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol index e2e187038ca1..3b7c0f9dce34 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol @@ -20,5 +20,4 @@ contract C { // SMTIgnoreCex: yes // ---- // Warning 6328: (258-274): CHC: Assertion violation happens here. -// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. -// Warning 1236: (33-46): BMC: Insufficient funds happens here. +// Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol index f16a57acf68f..826af0bf867d 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol @@ -23,5 +23,4 @@ contract C { // SMTIgnoreCex: yes // ---- // Warning 6328: (315-331): CHC: Assertion violation happens here. -// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. -// Warning 1236: (87-100): BMC: Insufficient funds happens here. +// Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol index 4b500581d323..02e29be8de9c 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol @@ -21,6 +21,6 @@ contract C { // SMTIgnoreCex: yes // ---- // Warning 4588: (238-243): Assertion checker does not yet implement this type of function call. +// Warning 8656: (54-67): CHC: Insufficient funds happens here. // Warning 6328: (282-298): CHC: Assertion violation happens here. // Warning 6328: (317-331): CHC: Assertion violation happens here. -// Warning 1236: (54-67): BMC: Insufficient funds happens here. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol b/test/libsolidity/smtCheckerTests/blockchain_state/transfer_1.sol similarity index 66% rename from test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol rename to test/libsolidity/smtCheckerTests/blockchain_state/transfer_1.sol index c099ffb2e5c9..3118086b921a 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/transfer_1.sol @@ -12,5 +12,4 @@ contract C { // SMTIgnoreCex: yes // ---- // Warning 6328: (166-201): CHC: Assertion violation happens here. -// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. -// Info 6002: BMC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. \ No newline at end of file diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/transfer_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/transfer_2.sol new file mode 100644 index 000000000000..ed5b4c90f2cf --- /dev/null +++ b/test/libsolidity/smtCheckerTests/blockchain_state/transfer_2.sol @@ -0,0 +1,14 @@ +contract C { + address payable recipient; + uint amount; + + function shouldHold() public { + uint tempAmount = address(this).balance; + recipient.transfer(tempAmount); + recipient.transfer(amount); + } +} +// ==== +// SMTEngine: chc +// ---- +// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/transfer_3.sol b/test/libsolidity/smtCheckerTests/blockchain_state/transfer_3.sol new file mode 100644 index 000000000000..4b3318b6bece --- /dev/null +++ b/test/libsolidity/smtCheckerTests/blockchain_state/transfer_3.sol @@ -0,0 +1,11 @@ +contract C { + address payable recipient; + + function shouldFail() public { + recipient.transfer(1); + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 8656: (76-97): CHC: Insufficient funds happens here. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/transfer_4.sol b/test/libsolidity/smtCheckerTests/blockchain_state/transfer_4.sol new file mode 100644 index 000000000000..ab0c4a81efeb --- /dev/null +++ b/test/libsolidity/smtCheckerTests/blockchain_state/transfer_4.sol @@ -0,0 +1,12 @@ +contract C { + address payable recipient; + + function f() public payable { + require(msg.value > 1); + recipient.transfer(1); + } +} +// ==== +// SMTEngine: all +// ---- +// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/functions/this_state.sol b/test/libsolidity/smtCheckerTests/functions/this_state.sol index dec101060d8c..d069bd90f8e1 100644 --- a/test/libsolidity/smtCheckerTests/functions/this_state.sol +++ b/test/libsolidity/smtCheckerTests/functions/this_state.sol @@ -1,14 +1,14 @@ contract C { - uint public x; - function g() public { + uint public x; + function g() public { x = 0; - this.h(); + this.h(); assert(x == 2); - } - function h() public { - x = 2; - } + } + function h() public { + x = 2; + } } // ==== // SMTEngine: all diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer.sol b/test/libsolidity/smtCheckerTests/types/address_transfer.sol index 89e8ae10274e..1430e15cb8e7 100644 --- a/test/libsolidity/smtCheckerTests/types/address_transfer.sol +++ b/test/libsolidity/smtCheckerTests/types/address_transfer.sol @@ -11,5 +11,5 @@ contract C // ==== // SMTEngine: all // ---- +// Warning 8656: (98-113): CHC: Insufficient funds happens here. // Warning 6328: (162-186): CHC: Assertion violation happens here. -// Warning 1236: (98-113): BMC: Insufficient funds happens here. diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol b/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol index 0a2c08d0caab..ce6492d9e57a 100644 --- a/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol +++ b/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol @@ -15,6 +15,6 @@ contract C // SMTEngine: all // SMTIgnoreCex: yes // ---- +// Warning 8656: (184-199): CHC: Insufficient funds happens here. +// Warning 8656: (203-218): CHC: Insufficient funds happens here. // Warning 6328: (262-291): CHC: Assertion violation happens here. -// Warning 1236: (184-199): BMC: Insufficient funds happens here. -// Warning 1236: (203-218): BMC: Insufficient funds happens here. diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer_3.sol b/test/libsolidity/smtCheckerTests/types/address_transfer_3.sol index 02d20c4f5bc4..3f9cc22c7bd6 100644 --- a/test/libsolidity/smtCheckerTests/types/address_transfer_3.sol +++ b/test/libsolidity/smtCheckerTests/types/address_transfer_3.sol @@ -13,5 +13,4 @@ contract C // ==== // SMTEngine: all // ---- -// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. -// Info 6002: BMC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. +// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol b/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol index 59568cb5be91..55a96026ee51 100644 --- a/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol +++ b/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol @@ -12,6 +12,6 @@ contract C // SMTEngine: all // SMTIgnoreCex: yes // ---- +// Warning 8656: (101-116): CHC: Insufficient funds happens here. +// Warning 8656: (120-136): CHC: Insufficient funds happens here. // Warning 6328: (180-204): CHC: Assertion violation happens here. -// Warning 1236: (101-116): BMC: Insufficient funds happens here. -// Warning 1236: (120-136): BMC: Insufficient funds happens here.