diff --git a/Changelog.md b/Changelog.md index ae3122813..223c692dd 100644 --- a/Changelog.md +++ b/Changelog.md @@ -8,10 +8,10 @@ Compiler Features: Bugfixes: * SMTChecker: Fix internal error on ``FixedBytes`` constant initialized with string literal. + * SMTChecker: Fix internal error on calling public getter on a state variable of type array (possibly nested) of structs. * SMTChecker: Fix internal error on pushing to ``string`` casted to ``bytes``. AST Changes: - ### 0.8.2 (2021-03-02) Compiler Features: diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 3afa40160..b7c864d1c 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -35,6 +35,8 @@ #include #include +#include + using namespace std; using namespace solidity; using namespace solidity::util; @@ -1016,60 +1018,71 @@ void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall) auto paramExpectedTypes = FunctionType(*var).parameterTypes(); auto actualArguments = _funCall.arguments(); solAssert(actualArguments.size() == paramExpectedTypes.size(), ""); - vector symbArguments; + deque symbArguments; for (unsigned i = 0; i < paramExpectedTypes.size(); ++i) symbArguments.push_back(expr(*actualArguments[i], paramExpectedTypes[i])); + // See FunctionType::FunctionType(VariableDeclaration const& _varDecl) + // to understand the return types of public getters. TypePointer type = var->type(); - if ( - type->isValueType() || - (type->category() == Type::Category::Array && dynamic_cast(*type).isByteArray()) - ) + smtutil::Expression currentExpr = currentValue(*var); + while (true) { - solAssert(symbArguments.empty(), ""); - defineExpr(_funCall, currentValue(*var)); - return; - } - switch (type->category()) - { - case Type::Category::Array: - case Type::Category::Mapping: + if ( + type->isValueType() || + (type->category() == Type::Category::Array && dynamic_cast(*type).isByteArray()) + ) { - // For nested arrays/mappings, each argument in the call is an index to the next layer. - // We mirror this with `select` after unpacking the SMT-LIB array expression. - smtutil::Expression exprVal = currentValue(*var); - for (auto const& arg: symbArguments) - { - exprVal = smtutil::Expression::select( - smtutil::Expression::tuple_get(exprVal, 0), - arg - ); - } - defineExpr(_funCall, exprVal); - break; + solAssert(symbArguments.empty(), ""); + defineExpr(_funCall, currentExpr); + return; } - case Type::Category::Struct: + switch (type->category()) { - auto returnedMembers = structGetterReturnedMembers(dynamic_cast(*type)); - solAssert(!returnedMembers.empty(), ""); - auto structVar = dynamic_pointer_cast(m_context.variable(*var)); - solAssert(structVar, ""); - auto returnedValues = applyMap(returnedMembers, [&](string const& memberName) { return structVar->member(memberName); }); - if (returnedValues.size() == 1) - defineExpr(_funCall, returnedValues.front()); - else + case Type::Category::Array: + case Type::Category::Mapping: { - auto symbTuple = dynamic_pointer_cast(m_context.expression(_funCall)); - solAssert(symbTuple, ""); - symbTuple->increaseIndex(); // Increasing the index explicitly since we cannot use defineExpr in this case. - auto const& symbComponents = symbTuple->components(); - solAssert(symbComponents.size() == returnedValues.size(), ""); - for (unsigned i = 0; i < symbComponents.size(); ++i) - m_context.addAssertion(symbTuple->component(i) == returnedValues.at(i)); + solAssert(!symbArguments.empty(), ""); + // For nested arrays/mappings, each argument in the call is an index to the next layer. + // We mirror this with `select` after unpacking the SMT-LIB array expression. + currentExpr = smtutil::Expression::select(smtutil::Expression::tuple_get(currentExpr, 0), symbArguments.front()); + symbArguments.pop_front(); + if (auto arrayType = dynamic_cast(type)) + type = arrayType->baseType(); + else if (auto mappingType = dynamic_cast(type)) + type = mappingType->valueType(); + else + solAssert(false, ""); + break; + } + case Type::Category::Struct: + { + solAssert(symbArguments.empty(), ""); + smt::SymbolicStructVariable structVar(dynamic_cast(type), "struct_temp_" + to_string(_funCall.id()), m_context); + m_context.addAssertion(structVar.currentValue() == currentExpr); + auto returnedMembers = structGetterReturnedMembers(dynamic_cast(*structVar.type())); + solAssert(!returnedMembers.empty(), ""); + auto returnedValues = applyMap(returnedMembers, [&](string const& memberName) { return structVar.member(memberName); }); + if (returnedValues.size() == 1) + defineExpr(_funCall, returnedValues.front()); + else + { + auto symbTuple = dynamic_pointer_cast(m_context.expression(_funCall)); + solAssert(symbTuple, ""); + symbTuple->increaseIndex(); // Increasing the index explicitly since we cannot use defineExpr in this case. + auto const& symbComponents = symbTuple->components(); + solAssert(symbComponents.size() == returnedValues.size(), ""); + for (unsigned i = 0; i < symbComponents.size(); ++i) + m_context.addAssertion(symbTuple->component(i) == returnedValues.at(i)); + } + return; + } + default: + { + // Unsupported cases, do nothing and the getter will be abstracted. + return; } - break; } - default: {} // Unsupported cases, do nothing and the getter will be abstracted. } } diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 5b347ec5c..f69f45146 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -311,7 +311,6 @@ protected: void createExpr(Expression const& _e); /// Creates the expression and sets its value. void defineExpr(Expression const& _e, smtutil::Expression _value); - /// Overwrites the current path condition void setPathCondition(smtutil::Expression const& _e); /// Adds a new path condition diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_1.sol new file mode 100644 index 000000000..688cf0783 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_1.sol @@ -0,0 +1,16 @@ +pragma abicoder v1; +pragma experimental SMTChecker; + +struct Item { + uint x; + uint y; +} + +contract D { + Item[][][] public items; + + function test() public view returns (uint) { + (uint a, uint b) = this.items(1, 2, 3); + return a + b; + } +} diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_2.sol new file mode 100644 index 000000000..bb13caf9f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_2.sol @@ -0,0 +1,22 @@ +pragma abicoder v1; +pragma experimental SMTChecker; + +struct Item { + uint x; + uint y; +} + +contract D { + Item[] public items; + + function test() public { + delete items; + items.push(Item(42, 43)); + (uint a, uint b) = this.items(0); + assert(a == 42); // should hold + assert(b == 43); // should hold + assert(b == 0); // should fail + } +} +// ---- +// Warning 6328: (300-314): CHC: Assertion violation happens here.\nCounterexample:\nitems = [{x: 42, y: 43}]\n\nTransaction trace:\nD.constructor()\nState: items = []\nD.test() diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_3.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_3.sol new file mode 100644 index 000000000..70875edf8 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_3.sol @@ -0,0 +1,24 @@ +pragma abicoder v1; +pragma experimental SMTChecker; + +struct Item { + uint x; + uint y; + uint[] arr; +} + +contract D { + Item[] public items; + + function test() public { + delete items; + uint[] memory tmp = new uint[](1); + items.push(Item(42, 43, tmp)); + (uint a, uint b) = this.items(0); + assert(a == 42); // should hold + assert(b == 43); // should hold + assert(b == 0); // should fail + } +} +// ---- +// Warning 6328: (355-369): CHC: Assertion violation happens here.\nCounterexample:\nitems = [{x: 42, y: 43, arr: [0]}]\n\nTransaction trace:\nD.constructor()\nState: items = []\nD.test()