Skip to content

SMTChecker: Fix error that reports invalid number of verified checks #15191

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

Merged
blishko merged 1 commit into from
Jun 17, 2024
Merged

SMTChecker: Fix error that reports invalid number of verified checks #15191

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.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Changelog.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ Compiler Features:


Bugfixes:
* SMTChecker: Fix error that reports invalid number of verified checks for BMC engine.
* TypeChecker: Fix segfault when assigning nested tuple to tuple.
* Yul Optimizer: Name simplification could lead to forbidden identifiers with a leading and/or trailing dot, e.g., ``x._`` would get simplified into ``x.``.

Expand Down
7 changes: 6 additions & 1 deletion libsolidity/formal/BMC.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -118,13 +118,18 @@ void BMC::analyze(SourceUnit const& _source, std::map<ASTNode const*, std::set<V
);

if (!m_settings.showProvedSafe && !m_safeTargets.empty())
{
std::size_t provedSafeNum = 0;
for (auto&& [_, targets]: m_safeTargets)
provedSafeNum += targets.size();
m_errorReporter.info(
6002_error,
"BMC: " +
std::to_string(m_safeTargets.size()) +
std::to_string(provedSafeNum) +
" verification condition(s) proved safe!" +
" Enable the model checker option \"show proved safe\" to see all of them."
);
}
else if (m_settings.showProvedSafe)
for (auto const& [node, targets]: m_safeTargets)
for (auto const& target: targets)
Expand Down
5 changes: 4 additions & 1 deletion libsolidity/formal/BMC.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,10 @@ class BMC: public SMTEncoder

friend bool operator<(BMCVerificationTarget const& _a, BMCVerificationTarget const& _b)
{
return _a.expression->id() < _b.expression->id();
if (_a.expression->id() == _b.expression->id())
Copy link
Contributor Author

@pgebal pgebal Jun 11, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here was the problem. We didn't accumulate more than 1 proved BMC target for a given expression.

Copy link
Collaborator

@blishko blishko Jun 13, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Right, good catch!

return _a.type < _b.type;
else
return _a.expression->id() < _b.expression->id();
}
};

Expand Down
2 changes: 1 addition & 1 deletion ...ity/smtCheckerTests/bmc_coverage/branches_with_return/constructor_state_variable_init.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,4 +39,4 @@ contract C is B {
// Warning 4661: (389-412): BMC: Assertion violation happens here.
// Warning 4661: (489-513): BMC: Assertion violation happens here.
// Warning 4661: (533-546): BMC: Assertion violation happens here.
// Info 6002: BMC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
// Info 6002: BMC: 5 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/operators/unary_minus_bmc.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,4 +8,4 @@ contract C
// SMTEngine: bmc
// ----
// Warning 4661: (48-63): BMC: Assertion violation happens here.
// Info 6002: BMC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
// Info 6002: BMC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
2 changes: 1 addition & 1 deletion ...kerTests/operators/userDefined/user_defined_operator_matches_equivalent_function_call.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,4 +77,4 @@ contract C {
// Warning 4144: (953-982): BMC: Underflow (resulting value less than -32768) happens here.
// Warning 3046: (1149-1178): BMC: Division by zero happens here.
// Warning 7812: (2245-2271): BMC: Assertion violation might happen here.
// Info 6002: BMC: 8 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
// Info 6002: BMC: 10 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/overflow/overflow_and_underflow_bmc.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
contract C {
function f(int x, int y) public pure returns (int) {
require(x == 0);
require(y == 0);
return x + y;
}
}
// ====
// SMTEngine: bmc
// ----
// Info 6002: BMC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.