From 547a6915ad0e439689205842400914e0a5a72345 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Tue, 1 Jun 2021 13:12:46 +0200 Subject: [PATCH] Fix ICE on external calls from constructor --- Changelog.md | 1 + libsolidity/formal/CHC.cpp | 9 ++++---- .../external_call_from_constructor_1.sol | 19 +++++++++++++++ .../external_call_from_constructor_2.sol | 16 +++++++++++++ .../external_call_from_constructor_3.sol | 23 +++++++++++++++++++ .../imports/import_as_module_1.sol | 2 +- .../imports/import_as_module_2.sol | 10 ++++---- 7 files changed, 69 insertions(+), 11 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol diff --git a/Changelog.md b/Changelog.md index faab15472..95fac0730 100644 --- a/Changelog.md +++ b/Changelog.md @@ -17,6 +17,7 @@ Compiler Features: Bugfixes: * AST: Do not output value of Yul literal if it is not a valid UTF-8 string. * SMTChecker: Fix internal error on struct constructor with fixed bytes member initialized with string literal. + * SMTChecker: Fix internal error on external calls from the constructor. * Source Locations: Properly set source location of scoped blocks. * Standard JSON: Properly allow the ``inliner`` setting under ``settings.optimizer.details``. * Type Checker: Fix internal compiler error related to having mapping types in constructor parameter for abstract contracts. diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index ba2d68a75..23967ecd2 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -773,10 +773,10 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall) 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. - solAssert(m_currentContract && m_currentFunction, ""); - for (auto const* definedFunction: contractFunctions(*m_currentContract)) - if (!definedFunction->isConstructor() && definedFunction->isPublic()) - m_callGraph[m_currentFunction].insert(definedFunction); + if (m_currentFunction) + for (auto const* definedFunction: contractFunctions(*m_currentContract)) + if (!definedFunction->isConstructor() && definedFunction->isPublic()) + m_callGraph[m_currentFunction].insert(definedFunction); m_context.addAssertion(errorFlag().currentValue() == 0); } @@ -788,7 +788,6 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall) auto kind = funType.kind(); solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, ""); - solAssert(m_currentContract, ""); auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract); if (!function) return; diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1.sol new file mode 100644 index 000000000..3cdf5d156 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1.sol @@ -0,0 +1,19 @@ +contract State { + function f(uint _x) public pure returns (uint) { + assert(_x < 100); + return _x; + } +} +contract C { + State s; + uint z = s.f(2); + + function f() public view { + assert(z == 2); // should fail since we don't trust s.f's code + } +} +// ==== +// 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() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2.sol new file mode 100644 index 000000000..cfd56271b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2.sol @@ -0,0 +1,16 @@ +contract C { + uint z = this.g(2); + + function g(uint _x) public pure returns (uint) { + assert(_x > 0); + return _x; + } + + function f() public view { + assert(z == 2); // should fail since we don't trust s.f's code + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\nz = 2\n_x = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: z = 2\nC.g(0) diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol new file mode 100644 index 000000000..eb5cd97dd --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol @@ -0,0 +1,23 @@ +contract State { + function f(uint _x) public pure returns (uint) { + assert(_x < 100); + return _x; + } +} +contract C { + State s; + uint z; + + constructor() { + z = s.f(2); + } + + function f() public view { + assert(z == 2); // should fail since we don't trust s.f's code + } +} +// ==== +// 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 = 3\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 3\nC.f() diff --git a/test/libsolidity/smtCheckerTests/imports/import_as_module_1.sol b/test/libsolidity/smtCheckerTests/imports/import_as_module_1.sol index e0d0ecf00..7796d3a9a 100644 --- a/test/libsolidity/smtCheckerTests/imports/import_as_module_1.sol +++ b/test/libsolidity/smtCheckerTests/imports/import_as_module_1.sol @@ -17,4 +17,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (117-132): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n_y = 0\n\nTransaction trace:\nD.constructor()\nState: x = 0\nD.f(0)\n C.g(0) -- internal call +// Warning 6328: (A:117-132): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n_y = 0\n\nTransaction trace:\nD.constructor()\nState: x = 0\nD.f(0)\n C.g(0) -- internal call diff --git a/test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol b/test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol index 93a3ecc1d..5288bd99c 100644 --- a/test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol +++ b/test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol @@ -18,9 +18,9 @@ function f(uint _x) pure { // ==== // SMTEngine: all // ---- -// Warning 8364: (118-119): Assertion checker does not yet implement type module "s1.sol" -// Warning 8364: (145-146): Assertion checker does not yet implement type module "s1.sol" -// Warning 6328: (50-64): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n s1.sol:f(200) -- internal call\n s1.sol:f(0) -- internal call\n f(10) -- internal call\n f(0) -- internal call +// Warning 8364: (A:118-119): Assertion checker does not yet implement type module "s1.sol" +// Warning 8364: (A:145-146): Assertion checker does not yet implement type module "s1.sol" +// Warning 6328: (A:50-64): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n s1.sol:f(200) -- internal call\n s1.sol:f(0) -- internal call\n A:f(10) -- internal call\n A:f(0) -- internal call // Warning 6328: (s1.sol:28-44): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n s1.sol:f(200) -- internal call\n s1.sol:f(0) -- internal call -// Warning 8364: (118-119): Assertion checker does not yet implement type module "s1.sol" -// Warning 8364: (145-146): Assertion checker does not yet implement type module "s1.sol" +// Warning 8364: (A:118-119): Assertion checker does not yet implement type module "s1.sol" +// Warning 8364: (A:145-146): Assertion checker does not yet implement type module "s1.sol"