cerc-io/solidity
16
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] Do not create targets for contracts that cannot be deployed

Browse Source
This commit is contained in:
Martin Blicha 2021-03-19 10:53:16 +01:00
parent 7e1be52281
commit 85358dfe30
10 changed files with 35 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -10,6 +10,7 @@ Compiler Features:
Bugfixes:
* AST Output: Fix ``kind`` field of ``ModifierInvocation`` for base constructor calls.
* SMTChecker: Fix false positive and false negative on ``push`` as LHS of a compound assignment.
* SMTChecker: Fix false positive in contracts that cannot be deployed.
* SMTChecker: Fix internal error on public getter returning dynamic data on older EVM versions where these are not available.

2
libsolidity/formal/BMC.cpp
View File

@ -841,7 +841,7 @@ void BMC::addVerificationTarget(
Expression const* _expression
)
{
if (!m_settings.targets.has(_type))
if (!m_settings.targets.has(_type) || (m_currentContract && !m_currentContract->canBeDeployed()))
return;
BMCVerificationTarget target{

19
libsolidity/formal/CHC.cpp
View File

@ -197,13 +197,17 @@ void CHC::endVisit(ContractDefinition const& _contract)
connectBlocks(m_currentBlock, summary(_contract));
setCurrentBlock(*m_constructorSummaries.at(&_contract));
auto constructor = _contract.constructor();
auto txConstraints = state().txTypeConstraints();
if (!constructor || !constructor->isPayable())
txConstraints = txConstraints && state().txNonPayableConstraint();
m_queryPlaceholders[&_contract].push_back({txConstraints, errorFlag().currentValue(), m_currentBlock});
connectBlocks(m_currentBlock, interface(), txConstraints && errorFlag().currentValue() == 0);
solAssert(&_contract == m_currentContract, "");
if (_contract.canBeDeployed())
{
auto constructor = _contract.constructor();
auto txConstraints = state().txTypeConstraints();
if (!constructor || !constructor->isPayable())
txConstraints = txConstraints && state().txNonPayableConstraint();
m_queryPlaceholders[&_contract].push_back({txConstraints, errorFlag().currentValue(), m_currentBlock});
connectBlocks(m_currentBlock, interface(), txConstraints && errorFlag().currentValue() == 0);
}
SMTEncoder::endVisit(_contract);
}
@ -262,7 +266,8 @@ void CHC::endVisit(FunctionDefinition const& _function)
if (
!_function.isConstructor() &&
_function.isPublic() &&
contractFunctions(*m_currentContract).count(&_function)
contractFunctions(*m_currentContract).count(&_function) &&
m_currentContract->canBeDeployed()
)
{
auto sum = summary(_function);

1
test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol
View File

@ -29,7 +29,6 @@ contract A is B2, B1 {
// ====
// SMTIgnoreCex: yes
// ----
// Warning 4984: (160-165): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (241-246): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (225-230): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (334-350): CHC: Assertion violation happens here.

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

@ -15,4 +15,4 @@ contract C is A {
}
}
// ----
// Warning 6328: (94-108): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()
// Warning 6328: (94-108): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.f()

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

@ -23,6 +23,6 @@ contract A is B {
// ====
// SMTIgnoreCex: yes
// ----
// Warning 4984: (157-162): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (275-293): CHC: Assertion violation happens here.
// Warning 4984: (157-162): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (216-221): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

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

@ -23,6 +23,6 @@ contract A is B {
// ====
// SMTIgnoreCex: yes
// ----
// Warning 4984: (157-163): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (273-291): CHC: Assertion violation happens here.
// Warning 4984: (157-163): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (217-222): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

9
test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol
View File

@ -4,7 +4,7 @@ abstract contract A {
int x = 0;
function f() public view mod() {
assert(x != 0); // fails for A
assert(x != 0); // does not hold for A, but A is abstract so it should not be reported
assert(x != 1); // fails for B
assert(x != 2); // fails for C
assert(x != 3); // fails for D
@ -36,7 +36,6 @@ contract D is B,C {
}
}
// ----
// Warning 6328: (104-118): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()
// Warning 6328: (137-151): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nB.constructor()\nState: x = 0\nA.f()
// Warning 6328: (170-184): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.f()
// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nD.constructor()\nState: x = 0\nA.f()
// Warning 6328: (193-207): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nB.constructor()\nState: x = 0\nA.f()
// Warning 6328: (226-240): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.f()
// Warning 6328: (259-273): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nD.constructor()\nState: x = 0\nA.f()

7
test/libsolidity/smtCheckerTests/verification_target/no_target_for_abstract_constract.sol Normal file
View File

@ -0,0 +1,7 @@
pragma experimental SMTChecker;
abstract contract A {
function f() public pure {
assert(false); // A cannot be deployed so this should not be reported
}
}

7
test/libsolidity/smtCheckerTests/verification_target/no_target_for_constructor_of_abstract_constract.sol Normal file
View File

@ -0,0 +1,7 @@
pragma experimental SMTChecker;
abstract contract A {
constructor() {
assert(false); // A cannot be deployed, so this should not be reported
}
}