cerc-io/solidity
15
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

[SMTChecker] Merge all entry points for a target

Browse Source
This commit is contained in:
Leo Alt 2021-10-20 16:21:34 +02:00
parent a7b137829f
commit e40cf92b1d
10 changed files with 24 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
libsolidity/formal/CHC.cpp
View File

@ -1623,28 +1623,23 @@ void CHC::checkVerificationTargets()
// Also, all possible contexts in which an external function can be called has been recorded (m_queryPlaceholders).
// Here we combine every context in which an external function can be called with all possible verification conditions
// in its call graph. Each such combination forms a unique verification target.
vector<CHCVerificationTarget> verificationTargets;
map<unsigned, vector<CHCQueryPlaceholder>> targetEntryPoints;
for (auto const& [function, placeholders]: m_queryPlaceholders)
{
auto functionTargets = transactionVerificationTargetsIds(function);
for (auto const& placeholder: placeholders)
for (unsigned id: functionTargets)
{
auto const& target = m_verificationTargets.at(id);
verificationTargets.push_back(CHCVerificationTarget{
{target.type, placeholder.fromPredicate, placeholder.constraints && placeholder.errorExpression == target.errorId},
target.errorId,
target.errorNode
});
}
targetEntryPoints[id].push_back(placeholder);
}
set<unsigned> checkedErrorIds;
for (auto const& target: verificationTargets)
for (auto const& [targetId, placeholders]: targetEntryPoints)
{
string errorType;
ErrorId errorReporterId;
auto const& target = m_verificationTargets.at(targetId);
if (target.type == VerificationTargetType::PopEmptyArray)
{
solAssert(dynamic_cast<FunctionCall const*>(target.errorNode), "");
@ -1692,7 +1687,7 @@ void CHC::checkVerificationTargets()
else
solAssert(false, "");
checkAndReportTarget(target, errorReporterId, errorType + " happens here.", errorType + " might happen here.");
checkAndReportTarget(target, placeholders, errorReporterId, errorType + " happens here.", errorType + " might happen here.");
checkedErrorIds.insert(target.errorId);
}
@ -1750,7 +1745,7 @@ void CHC::checkVerificationTargets()
{
set<unsigned> seenErrors;
msg += "<errorCode> = 0 -> no errors\n";
for (auto const& target: verificationTargets)
for (auto const& [id, target]: m_verificationTargets)
if (!seenErrors.count(target.errorId))
{
seenErrors.insert(target.errorId);
@ -1785,6 +1780,7 @@ void CHC::checkVerificationTargets()
void CHC::checkAndReportTarget(
CHCVerificationTarget const& _target,
vector<CHCQueryPlaceholder> const& _placeholders,
ErrorId _errorReporterId,
string _satMsg,
string _unknownMsg
@ -1794,7 +1790,12 @@ void CHC::checkAndReportTarget(
return;
createErrorBlock();
connectBlocks(_target.value, error(), _target.constraints);
for (auto const& placeholder: _placeholders)
connectBlocks(
placeholder.fromPredicate,
error(),
placeholder.constraints && placeholder.errorExpression == _target.errorId
);
auto const& location = _target.errorNode->location();
auto [result, invariant, model] = query(error(), location);
if (result == CheckResult::UNSATISFIABLE)

4
libsolidity/formal/CHC.h
View File

@ -252,11 +252,13 @@ private:
void verificationTargetEncountered(ASTNode const* const _errorNode, VerificationTargetType _type, smtutil::Expression const& _errorCondition);
void checkVerificationTargets();
// Forward declaration. Definition is below.
// Forward declarations. Definitions are below.
struct CHCVerificationTarget;
struct CHCQueryPlaceholder;
void checkAssertTarget(ASTNode const* _scope, CHCVerificationTarget const& _target);
void checkAndReportTarget(
CHCVerificationTarget const& _target,
std::vector<CHCQueryPlaceholder> const& _placeholders,
langutil::ErrorId _errorReporterId,
std::string _satMsg,
std::string _unknownMsg = ""

1
test/cmdlineTests/model_checker_invariants_all/err
View File

@ -7,7 +7,6 @@ Warning: Return value of low-level calls not used.
Info: Contract invariant(s) for model_checker_invariants_all/input.sol:test:
(x <= 0)
Reentrancy property(ies) for model_checker_invariants_all/input.sol:test:
(!(x <= 0) || (x' <= 0))
((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
<errorCode> = 0 -> no errors

1
test/cmdlineTests/model_checker_invariants_contract_reentrancy/err
View File

@ -7,7 +7,6 @@ Warning: Return value of low-level calls not used.
Info: Contract invariant(s) for model_checker_invariants_contract_reentrancy/input.sol:test:
(x <= 0)
Reentrancy property(ies) for model_checker_invariants_contract_reentrancy/input.sol:test:
(!(x <= 0) || (x' <= 0))
((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
<errorCode> = 0 -> no errors

2
test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json
View File

@ -7,7 +7,6 @@
","message":"Return value of low-level calls not used.","severity":"warning","sourceLocation":{"end":143,"file":"A","start":132},"type":"Warning"},{"component":"general","errorCode":"1180","formattedMessage":"Info: Contract invariant(s) for A:test:
(x <= 0)
Reentrancy property(ies) for A:test:
(!(x <= 0) || (x' <= 0))
((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
<errorCode> = 0 -> no errors
@ -18,7 +17,6 @@ Reentrancy property(ies) for A:test:
","message":"Contract invariant(s) for A:test:
(x <= 0)
Reentrancy property(ies) for A:test:
(!(x <= 0) || (x' <= 0))
((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
<errorCode> = 0 -> no errors

2
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol
View File

@ -25,8 +25,8 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreInv: yes
// ----
// Warning 1218: (302-333): CHC: Error trying to invoke SMT solver.
// Warning 6328: (302-333): CHC: Assertion violation might happen here.
// Info 1180: Contract invariant(s) for :C:\n(((kec + ((- 1) * keccak256(data))) >= 0) && ((kec + ((- 1) * keccak256(data))) <= 0))\nReentrancy property(ies) for :C:\n((!((kec + ((- 1) * keccak256(data))) >= 0) || ((kec' + ((- 1) * keccak256(data'))) >= 0)) && (!((kec + ((- 1) * keccak256(data))) <= 0) || ((kec' + ((- 1) * keccak256(data'))) <= 0)))\n((!(<errorCode> = 1) || !((kec + ((- 1) * keccak256(data))) = 0)) && (!((kec + ((- 1) * keccak256(data))) <= 0) || ((kec' + ((- 1) * keccak256(data'))) <= 0)) && (!((kec + ((- 1) * keccak256(data))) >= 0) || ((kec' + ((- 1) * keccak256(data'))) >= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(_kec == kec)\n<errorCode> = 2 -> Assertion failed at assert(kec == keccak256(_data))\n
// Warning 4661: (302-333): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol
View File

@ -15,5 +15,5 @@ contract C is B {
// ====
// SMTEngine: all
// ----
// Warning 6328: (52-66): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 1\n\nTransaction trace:\nC.constructor()\nState: y = 0, x = 0\nC.g()\n B.f() -- internal call\nState: y = 0, x = 1\nB.f()
// Warning 6328: (52-66): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 1\n\nTransaction trace:\nC.constructor()\nState: y = 0, x = 0\nC.g()\n B.f() -- internal call
// Info 1180: Contract invariant(s) for :B:\n(x <= 0)\n

3
test/libsolidity/smtCheckerTests/inheritance/implicit_constructor_hierarchy.sol
View File

@ -15,5 +15,4 @@ contract C is B {
// ====
// SMTEngine: all
// SMTSolvers: z3
// ----
// Info 1180: Contract invariant(s) for :C:\n(!(x <= 1) && !(x >= 3))\n
// SMTIgnoreInv: yes

4
test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol
View File

@ -25,4 +25,6 @@ contract C {
// SMTIgnoreCex: yes
// ----
// Warning 2072: (249-255): Unused local variable.
// Warning 6328: (271-295): CHC: Assertion violation happens here.
// Warning 1218: (271-295): CHC: Error trying to invoke SMT solver.
// Warning 6328: (271-295): CHC: Assertion violation might happen here.
// Warning 4661: (271-295): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol
View File

@ -25,4 +25,4 @@ contract C {
// SMTIgnoreOS: macos
// ----
// Warning 2072: (255-261): Unused local variable.
// Info 1180: Reentrancy property(ies) for :C:\n((!(x <= 2) || !(x' >= 3)) && (<errorCode> <= 0) && (!(x' <= 0) || !(x >= 2)))\n((!(x' <= 0) || ((x' + ((- 1) * x)) = 0)) && (<errorCode> <= 0) && (!(x' >= 3) || ((x' + ((- 1) * x)) = 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 2 || x == 1)\n
// Info 1180: Reentrancy property(ies) for :C:\n((!(x' <= 0) || ((x' + ((- 1) * x)) = 0)) && (<errorCode> <= 0) && (!(x' >= 3) || ((x' + ((- 1) * x)) = 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 2 || x == 1)\n