From c7ca87c012eecec76d3e311670ebb1eccfa09572 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 18 Jan 2021 11:40:04 +0100 Subject: [PATCH] Fix static virtual resolution --- libsolidity/formal/SMTEncoder.cpp | 15 ++++++++++--- .../overriden_function_static_call_parent.sol | 21 +++++++++++++++++++ 2 files changed, 33 insertions(+), 3 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/inheritance/overriden_function_static_call_parent.sol diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 45e6d7eb9..f11687898 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -2643,15 +2643,24 @@ pair SMTEncoder::functionC auto funDef = dynamic_cast(_ref->annotation().referencedDeclaration); if (!funDef) return {funDef, _contract}; - auto contextContract = _contract; - if (lookup == VirtualLookup::Virtual) + ContractDefinition const* contextContract = nullptr; + switch (lookup) + { + case VirtualLookup::Virtual: funDef = &funDef->resolveVirtual(*_contract); - else if (lookup == VirtualLookup::Super) + contextContract = _contract; + break; + case VirtualLookup::Super: { auto super = _contract->superContract(*_contract); solAssert(super, "Super contract not available."); funDef = &funDef->resolveVirtual(*_contract, super); contextContract = super; + break; + } + case VirtualLookup::Static: + contextContract = funDef->annotation().contract; + break; } return {funDef, contextContract}; }; diff --git a/test/libsolidity/smtCheckerTests/inheritance/overriden_function_static_call_parent.sol b/test/libsolidity/smtCheckerTests/inheritance/overriden_function_static_call_parent.sol new file mode 100644 index 000000000..81f32a009 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/overriden_function_static_call_parent.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; +contract BaseBase { + uint x; + function init(uint a, uint b) public virtual { + x = a; + } +} +contract Base is BaseBase { + function init(uint a, uint b) public override { + } +} +contract Child is Base { + function bInit(uint c, uint d) public { + BaseBase.init(c, d); + assert(x == c); + assert(x == d); // should fail + } +} +// ---- +// Warning 5667: (84-90): Unused function parameter. Remove or comment out the variable name to silence this warning. +// Warning 6328: (314-328): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\nc = 0\nd = 1\n\nTransaction trace:\nChild.constructor()\nState: x = 0\nChild.bInit(0, 1)\n BaseBase.init(0, 1) -- internal call