From 07870d031894505132843555652f88f4cdf45874 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Mon, 28 Nov 2022 18:45:50 +0100 Subject: [PATCH] Fix internal error in assignment chains that also assign to fully qualified state variables (, for example), where the contract expression is a tuble. --- Changelog.md | 1 + libsolidity/formal/SMTEncoder.cpp | 4 +++- .../assignment_chain_tuple_contract_1.sol | 10 +++++++++ .../assignment_chain_tuple_contract_2.sol | 13 +++++++++++ .../assignment_chain_tuple_contract_3.sol | 22 +++++++++++++++++++ 5 files changed, 49 insertions(+), 1 deletion(-) create mode 100644 test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_1.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_2.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_3.sol diff --git a/Changelog.md b/Changelog.md index 4ac7a0d26..a78a8a5c5 100644 --- a/Changelog.md +++ b/Changelog.md @@ -25,6 +25,7 @@ Bugfixes: * SMTChecker: Improved readability for large integers that are powers of two or almost powers of two in error messages. * SMTChecker: Fix internal error when a public library function is called internally. * SMTChecker: Fix internal error on multiple wrong SMTChecker natspec entries. + * SMTChecker: Fix internal error on chain assignments using static fully specified state variables. ### 0.8.17 (2022-09-08) diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 818ac9278..8d758e784 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -2757,7 +2757,9 @@ VariableDeclaration const* SMTEncoder::identifierToVariable(Expression const& _e } // But we are interested in "contract.var", because that is the same as just "var". if (auto const* memberAccess = dynamic_cast(&_expr)) - if (dynamic_cast(expressionToDeclaration(memberAccess->expression()))) + if (dynamic_cast(expressionToDeclaration( + *cleanExpression(memberAccess->expression()) + ))) if (auto const* varDecl = dynamic_cast(memberAccess->annotation().referencedDeclaration)) { solAssert(m_context.knownVariable(*varDecl), ""); diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_1.sol b/test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_1.sol new file mode 100644 index 000000000..a0fd84c93 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_1.sol @@ -0,0 +1,10 @@ +contract C { + string public name = (C).name = type(C).name; + + function f() external view { + assert(keccak256(bytes(name)) == keccak256(bytes("C"))); // should fail because SMTChecker doesn't support type(C).name + } +} +// ---- +// Warning 7507: (49-61): Assertion checker does not yet support this expression. +// Warning 6328: (105-160): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_2.sol b/test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_2.sol new file mode 100644 index 000000000..4c97f8a69 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_2.sol @@ -0,0 +1,13 @@ +contract C { + uint x = ((((C)))).x = ((C)).x = 2; + + function f() external view { + assert(x == 2); // should hold + } + + function g() external view { + assert(x != 2); // should fail + } +} +// ---- +// Warning 6328: (174-188): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 2\nC.g() diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_3.sol b/test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_3.sol new file mode 100644 index 000000000..08b87282e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_3.sol @@ -0,0 +1,22 @@ +contract C { + uint x = ((((C)))).x = ((C)).x = 2; + + function f() external view { + assert(x == 2); // should fail for D + } + + function g() external view { + assert(x != 2); // should fail for C + } +} + +contract D is C { + uint y = ((C)).x = 3; + + function h() external view { + assert(y == 3); // should hold + } +} +// ---- +// Warning 6328: (95-109): CHC: Assertion violation happens here.\nCounterexample:\ny = 3, x = 3\n\nTransaction trace:\nD.constructor()\nState: y = 3, x = 3\nC.f() +// Warning 6328: (180-194): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 2\nC.g()