Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

SMTChecker: add insufficient funds verification target for CHC engine #15086

Merged
merged 1 commit into from
May 14, 2024
+125 −91
Merged

SMTChecker: add insufficient funds verification target for CHC engine #15086

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
2 changes: 1 addition & 1 deletion Changelog.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
6 changes: 6 additions & 0 deletions libsolidity/formal/BMC.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
18 changes: 18 additions & 0 deletions libsolidity/formal/CHC.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -2013,6 +2029,8 @@ std::pair<std::string, ErrorId> 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);
}
Expand Down
14 changes: 2 additions & 12 deletions test/cmdlineTests/model_checker_targets_all_all_engines/err
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
2 changes: 2 additions & 0 deletions test/cmdlineTests/model_checker_targets_all_chc/err
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
1 change: 1 addition & 0 deletions test/cmdlineTests/model_checker_targets_balance_chc/err
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
14 changes: 2 additions & 12 deletions test/cmdlineTests/model_checker_targets_default_all_engines/err
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
2 changes: 2 additions & 0 deletions test/cmdlineTests/model_checker_targets_default_chc/err
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
12 changes: 12 additions & 0 deletions test/cmdlineTests/standard_model_checker_targets_balance_chc/output.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
49 changes: 10 additions & 39 deletions test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand All @@ -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": {
Expand Down
10 changes: 10 additions & 0 deletions test/cmdlineTests/standard_model_checker_targets_default_chc/output.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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": {
Expand Down
3 changes: 1 addition & 2 deletions test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
6 changes: 3 additions & 3 deletions test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
2 changes: 1 addition & 1 deletion test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
3 changes: 1 addition & 2 deletions test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
3 changes: 1 addition & 2 deletions test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
2 changes: 1 addition & 1 deletion test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
blishko marked this conversation as resolved.
Show resolved Hide resolved
// 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.
3 changes: 1 addition & 2 deletions ...heckerTests/blockchain_state/transfer.sol → ...ckerTests/blockchain_state/transfer_1.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
14 changes: 14 additions & 0 deletions test/libsolidity/smtCheckerTests/blockchain_state/transfer_2.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
11 changes: 11 additions & 0 deletions test/libsolidity/smtCheckerTests/blockchain_state/transfer_3.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
12 changes: 12 additions & 0 deletions test/libsolidity/smtCheckerTests/blockchain_state/transfer_4.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
14 changes: 7 additions & 7 deletions test/libsolidity/smtCheckerTests/functions/this_state.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
2 changes: 1 addition & 1 deletion test/libsolidity/smtCheckerTests/types/address_transfer.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
4 changes: 2 additions & 2 deletions test/libsolidity/smtCheckerTests/types/address_transfer_2.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
3 changes: 1 addition & 2 deletions test/libsolidity/smtCheckerTests/types/address_transfer_3.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
4 changes: 2 additions & 2 deletions test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.