From 85358dfe307167ffddcded3568e0536056647a2e Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Fri, 19 Mar 2021 10:53:16 +0100 Subject: [PATCH] [SMTChecker] Do not create targets for contracts that cannot be deployed --- Changelog.md | 1 + libsolidity/formal/BMC.cpp | 2 +- libsolidity/formal/CHC.cpp | 19 ++++++++++++------- .../constructor_hierarchy_diamond_3.sol | 1 - .../base_contract_assertion_fail_8.sol | 2 +- ...ctor_state_variable_init_chain_run_all.sol | 2 +- ...or_state_variable_init_chain_run_all_2.sol | 2 +- .../modifiers/modifier_overriding_4.sol | 9 ++++----- .../no_target_for_abstract_constract.sol | 7 +++++++ ..._for_constructor_of_abstract_constract.sol | 7 +++++++ 10 files changed, 35 insertions(+), 17 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/verification_target/no_target_for_abstract_constract.sol create mode 100644 test/libsolidity/smtCheckerTests/verification_target/no_target_for_constructor_of_abstract_constract.sol diff --git a/Changelog.md b/Changelog.md index 40d94142d..7f73f4f60 100644 --- a/Changelog.md +++ b/Changelog.md @@ -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. diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 2d970a8a1..17ad9f652 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -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{ diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 50cd7645c..92ff0254c 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -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); diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol index f0bfc37cc..6a9999272 100644 --- a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol +++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_diamond_3.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_8.sol b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_8.sol index e3fbbd082..426b97bba 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_8.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_8.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol index 886469d27..d497e33da 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol index 39b5b7824..50a751e39 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_chain_run_all_2.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol index 172f98fcf..a02ea10f5 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_overriding_4.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/verification_target/no_target_for_abstract_constract.sol b/test/libsolidity/smtCheckerTests/verification_target/no_target_for_abstract_constract.sol new file mode 100644 index 000000000..590ee6be6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/verification_target/no_target_for_abstract_constract.sol @@ -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 + } +} diff --git a/test/libsolidity/smtCheckerTests/verification_target/no_target_for_constructor_of_abstract_constract.sol b/test/libsolidity/smtCheckerTests/verification_target/no_target_for_constructor_of_abstract_constract.sol new file mode 100644 index 000000000..0f176def4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/verification_target/no_target_for_constructor_of_abstract_constract.sol @@ -0,0 +1,7 @@ +pragma experimental SMTChecker; + +abstract contract A { + constructor() { + assert(false); // A cannot be deployed, so this should not be reported + } +}