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

Merge pull request #11795 from ethereum/smt_fix_ext_constructor

Browse Source 
[SMTChecker] Fix false positive on external calls from constructors
This commit is contained in:
Leonardo 2021-08-12 19:34:57 +02:00 committed by GitHub
commit b0164bd2a4
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 22 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -7,6 +7,7 @@ Compiler Features:
Bugfixes:
* SMTChecker: Fix false positive in external calls from constructors.

4
libsolidity/formal/CHC.cpp
View File

@ -756,6 +756,9 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
for (auto var: function->returnParameters())
m_context.variable(*var)->increaseIndex();
if (!m_currentFunction || m_currentFunction->isConstructor())
return;
auto preCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall ||
function->stateMutability() == StateMutability::Pure ||
@ -787,6 +790,7 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
m_context.addAssertion(nondetCall);
solAssert(m_errorDest, "");
connectBlocks(m_currentBlock, predicate(*m_errorDest), errorFlag().currentValue() > 0);
// To capture the possibility of a reentrant call, we record in the call graph that the current function
// can call any of the external methods of the current contract.
if (m_currentFunction)

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

@ -16,4 +16,4 @@ contract C {
// SMTEngine: all
// ----
// Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100)
// Warning 6328: (177-191): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 3\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 3\nC.f()
// Warning 6328: (177-191): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 0\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 0\nC.f()

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

@ -20,4 +20,4 @@ contract C {
// SMTEngine: all
// ----
// Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100)
// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 0\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 0\nC.f()
// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 3\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 3\nC.f()

15
test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_reentrancy_1.sol Normal file
View File

@ -0,0 +1,15 @@
interface D {
function ext(C c) external returns (uint);
}
contract C {
uint x;
function s(uint _x) public { x = _x; }
constructor(D d) {
uint a = d.ext(this);
assert(x == 0); // should hold because there's no reentrancy from the constructor
assert(a == 2); // should fail
}
}
// ----
// Warning 6328: (253-267): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\nd = 0\na = 3\n\nTransaction trace:\nC.constructor(0)