diff --git a/Changelog.md b/Changelog.md index cfd281893..0409261c2 100644 --- a/Changelog.md +++ b/Changelog.md @@ -6,6 +6,7 @@ Language Features: Compiler Features: * Build system: Update the soljson.js build to emscripten 1.39.15 and boost 1.73.0 and include Z3 for integrated SMTChecker support without the callback mechanism. * SMTChecker: Support array ``length``. + * SMTChecker: Support array ``push`` and ``pop``. Bugfixes: diff --git a/docs/security-considerations.rst b/docs/security-considerations.rst index f899736aa..772fa7c1d 100644 --- a/docs/security-considerations.rst +++ b/docs/security-considerations.rst @@ -657,3 +657,14 @@ Notice that we do not clear knowledge about ``array`` and ``d`` because they are located in storage, even though they also have type ``uint[]``. However, if ``d`` was assigned, we would need to clear knowledge about ``array`` and vice-versa. + +Real World Assumptions +====================== + +Some scenarios can be expressed in Solidity and the EVM, but are expected to +never occur in practice. +One of such cases is the length of a dynamic storage array overflowing during a +push: If the ``push`` operation is applied to an array of length 2^256 - 1, its +length silently overflows. +However, this is unlikely to happen in practice, since the operations required +to grow the array to that point would take billions of years to execute. diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 1453df34f..f30959972 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -98,17 +98,45 @@ void CHC::analyze(SourceUnit const& _source) for (auto const& [scope, target]: m_verificationTargets) { - auto assertions = transactionAssertions(scope); - for (auto const* assertion: assertions) + if (target.type == VerificationTarget::Type::Assert) { + auto assertions = transactionAssertions(scope); + for (auto const* assertion: assertions) + { + createErrorBlock(); + connectBlocks(target.value, error(), target.constraints && (target.errorId == assertion->id())); + auto [result, model] = query(error(), assertion->location()); + // This should be fine but it's a bug in the old compiler + (void)model; + if (result == smt::CheckResult::UNSATISFIABLE) + m_safeAssertions.insert(assertion); + } + } + else if (target.type == VerificationTarget::Type::PopEmptyArray) + { + solAssert(dynamic_cast(scope), ""); createErrorBlock(); - connectBlocks(target.value, error(), target.constraints && (target.errorId == assertion->id())); - auto [result, model] = query(error(), assertion->location()); + connectBlocks(target.value, error(), target.constraints && (target.errorId == scope->id())); + auto [result, model] = query(error(), scope->location()); // This should be fine but it's a bug in the old compiler (void)model; - if (result == smt::CheckResult::UNSATISFIABLE) - m_safeAssertions.insert(assertion); + if (result != smt::CheckResult::UNSATISFIABLE) + { + string msg = "Empty array \"pop\" "; + if (result == smt::CheckResult::SATISFIABLE) + msg += "detected here."; + else + msg += "might happen here."; + m_unsafeTargets.insert(scope); + m_outerErrorReporter.warning( + 2529_error, + scope->location(), + msg + ); + } } + else + solAssert(false, ""); } } @@ -161,7 +189,7 @@ void CHC::endVisit(ContractDefinition const& _contract) auto stateExprs = vector{m_error.currentValue()} + currentStateVariables(); setCurrentBlock(*m_constructorSummaryPredicate, &stateExprs); - addVerificationTarget(m_currentContract, m_currentBlock, smt::Expression(true), m_error.currentValue()); + addAssertVerificationTarget(m_currentContract, m_currentBlock, smt::Expression(true), m_error.currentValue()); connectBlocks(m_currentBlock, interface(), m_error.currentValue() == 0); SMTEncoder::endVisit(_contract); @@ -256,7 +284,7 @@ void CHC::endVisit(FunctionDefinition const& _function) if (_function.isPublic()) { - addVerificationTarget(&_function, m_currentBlock, sum, assertionError); + addAssertVerificationTarget(&_function, m_currentBlock, sum, assertionError); connectBlocks(m_currentBlock, iface, sum && (assertionError == 0)); } } @@ -556,10 +584,34 @@ void CHC::unknownFunctionCall(FunctionCall const&) m_unknownFunctionCallSeen = true; } +void CHC::makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) +{ + FunctionType const& funType = dynamic_cast(*_arrayPop.expression().annotation().type); + solAssert(funType.kind() == FunctionType::Kind::ArrayPop, ""); + + auto memberAccess = dynamic_cast(&_arrayPop.expression()); + solAssert(memberAccess, ""); + auto symbArray = dynamic_pointer_cast(m_context.expression(memberAccess->expression())); + solAssert(symbArray, ""); + + auto previousError = m_error.currentValue(); + m_error.increaseIndex(); + + addArrayPopVerificationTarget(&_arrayPop, m_error.currentValue()); + connectBlocks( + m_currentBlock, + m_currentFunction->isConstructor() ? summary(*m_currentContract) : summary(*m_currentFunction), + currentPathConditions() && symbArray->length() <= 0 && m_error.currentValue() == _arrayPop.id() + ); + + m_context.addAssertion(m_error.currentValue() == previousError); +} + void CHC::resetSourceAnalysis() { m_verificationTargets.clear(); m_safeAssertions.clear(); + m_unsafeTargets.clear(); m_functionAssertions.clear(); m_callGraph.clear(); m_summaries.clear(); @@ -974,9 +1026,35 @@ pair> CHC::query(smt::Expression const& _query, return {result, values}; } -void CHC::addVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId) +void CHC::addVerificationTarget( + ASTNode const* _scope, + VerificationTarget::Type _type, + smt::Expression _from, + smt::Expression _constraints, + smt::Expression _errorId +) { - m_verificationTargets.emplace(_scope, CHCVerificationTarget{{VerificationTarget::Type::Assert, _from, _constraints}, _errorId}); + m_verificationTargets.emplace(_scope, CHCVerificationTarget{{_type, _from, _constraints}, _errorId}); +} + +void CHC::addAssertVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId) +{ + addVerificationTarget(_scope, VerificationTarget::Type::Assert, _from, _constraints, _errorId); +} + +void CHC::addArrayPopVerificationTarget(ASTNode const* _scope, smt::Expression _errorId) +{ + solAssert(m_currentContract, ""); + solAssert(m_currentFunction, ""); + + if (m_currentFunction->isConstructor()) + addVerificationTarget(_scope, VerificationTarget::Type::PopEmptyArray, summary(*m_currentContract), smt::Expression(true), _errorId); + else + { + auto iface = (*m_interfaces.at(m_currentContract))(initialStateVariables()); + auto sum = summary(*m_currentFunction); + addVerificationTarget(_scope, VerificationTarget::Type::PopEmptyArray, iface, sum, _errorId); + } } string CHC::uniquePrefix() diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 7fc752451..87f902732 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -78,6 +78,7 @@ private: void visitAssert(FunctionCall const& _funCall); void internalFunctionCall(FunctionCall const& _funCall); void unknownFunctionCall(FunctionCall const& _funCall); + void makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) override; //@} struct IdCompare @@ -182,7 +183,9 @@ private: /// @returns otherwise. std::pair> query(smt::Expression const& _query, langutil::SourceLocation const& _location); - void addVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId); + void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId); + void addAssertVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId); + void addArrayPopVerificationTarget(ASTNode const* _scope, smt::Expression _errorId); //@} /// Misc. @@ -245,6 +248,8 @@ private: /// Assertions proven safe. std::set m_safeAssertions; + /// Targets proven unsafe. + std::set m_unsafeTargets; //@} /// Control-flow. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 09c188435..44bec4d85 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -646,6 +646,12 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall) m_context.state().transfer(m_context.state().thisAddress(), expr(address), expr(*value)); break; } + case FunctionType::Kind::ArrayPush: + arrayPush(_funCall); + break; + case FunctionType::Kind::ArrayPop: + arrayPop(_funCall); + break; default: m_errorReporter.warning( 4588_error, @@ -905,16 +911,6 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) m_context ); } - else - { - auto const& name = _memberAccess.memberName(); - solAssert(name == "push" || name == "pop", ""); - m_errorReporter.warning( - 9098_error, - _memberAccess.location(), - "Assertion checker does not yet support array member \"" + name + "\"." - ); - } return false; } else @@ -1082,6 +1078,76 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c } } +void SMTEncoder::arrayPush(FunctionCall const& _funCall) +{ + auto memberAccess = dynamic_cast(&_funCall.expression()); + solAssert(memberAccess, ""); + auto symbArray = dynamic_pointer_cast(m_context.expression(memberAccess->expression())); + solAssert(symbArray, ""); + auto oldLength = symbArray->length(); + m_context.addAssertion(oldLength >= 0); + // Real world assumption: the array length is assumed to not overflow. + // This assertion guarantees that both the current and updated lengths have the above property. + m_context.addAssertion(oldLength + 1 < (smt::maxValue(*TypeProvider::uint256()) - 1)); + + auto const& arguments = _funCall.arguments(); + smt::Expression element = arguments.empty() ? + smt::zeroValue(_funCall.annotation().type) : + expr(*arguments.front()); + smt::Expression store = smt::Expression::store( + symbArray->elements(), + oldLength, + element + ); + symbArray->increaseIndex(); + m_context.addAssertion(symbArray->elements() == store); + m_context.addAssertion(symbArray->length() == oldLength + 1); + + if (arguments.empty()) + defineExpr(_funCall, element); + + arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue()); +} + +void SMTEncoder::arrayPop(FunctionCall const& _funCall) +{ + auto memberAccess = dynamic_cast(&_funCall.expression()); + solAssert(memberAccess, ""); + auto symbArray = dynamic_pointer_cast(m_context.expression(memberAccess->expression())); + solAssert(symbArray, ""); + + makeArrayPopVerificationTarget(_funCall); + + auto oldElements = symbArray->elements(); + auto oldLength = symbArray->length(); + m_context.addAssertion(oldLength > 0); + + symbArray->increaseIndex(); + m_context.addAssertion(symbArray->elements() == oldElements); + auto newLength = smt::Expression::ite( + oldLength == 0, + smt::maxValue(*TypeProvider::uint256()), + oldLength - 1 + ); + m_context.addAssertion(symbArray->length() == oldLength - 1); + + arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue()); +} + +void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smt::Expression const& _array) +{ + if (auto const* id = dynamic_cast(&_expr)) + { + auto varDecl = identifierToVariable(*id); + solAssert(varDecl, ""); + m_context.addAssertion(m_context.newValue(*varDecl) == _array); + } + else if (auto const* indexAccess = dynamic_cast(&_expr)) + arrayIndexAssignment(*indexAccess, _array); + else + solAssert(false, ""); +} + void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _expr, bool _increaseIndex) { if (!m_context.knownGlobalSymbol(_name)) diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 21bf094c0..f62f18558 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -137,6 +137,13 @@ protected: /// Handles assignment to SMT array index. void arrayIndexAssignment(Expression const& _expr, smt::Expression const& _rightHandSide); + void arrayPush(FunctionCall const& _funCall); + void arrayPop(FunctionCall const& _funCall); + void arrayPushPopAssign(Expression const& _expr, smt::Expression const& _array); + /// Allows BMC and CHC to create verification targets for popping + /// an empty array. + virtual void makeArrayPopVerificationTarget(FunctionCall const&) {} + /// Division expression in the given type. Requires special treatment because /// of rounding for signed division. smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type); @@ -240,7 +247,7 @@ protected: struct VerificationTarget { - enum class Type { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert } type; + enum class Type { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert, PopEmptyArray } type; smt::Expression value; smt::Expression constraints; }; diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_1_safe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_1_safe.sol new file mode 100644 index 000000000..34663d931 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/pop_1_safe.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; + +contract C { + uint[] a; + function f() public { + a.push(); + a.pop(); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_1_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_1_unsafe.sol new file mode 100644 index 000000000..e6f2273f8 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/pop_1_unsafe.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C { + uint[] a; + function f() public { + a.pop(); + } +} +// ---- +// Warning: (82-89): Empty array "pop" detected here. diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_2d_safe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_2d_safe.sol new file mode 100644 index 000000000..c67e91959 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/pop_2d_safe.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C { + uint[][] a; + function f() public { + a.push(); + a[0].push(); + a[0].pop(); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol new file mode 100644 index 000000000..1161ab92e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; + +contract C { + uint[][] a; + function f() public { + a.push(); + a[0].push(); + a[1].pop(); + } +} +// ---- +// Warning: (111-121): Empty array "pop" detected here. diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_constructor_safe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_constructor_safe.sol new file mode 100644 index 000000000..4842ee56f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/pop_constructor_safe.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; + +contract C { + uint[] a; + constructor() public { + a.push(); + a.pop(); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol new file mode 100644 index 000000000..a86d1a3f3 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C { + uint[] a; + constructor() public { + a.pop(); + } +} +// ---- +// Warning: (83-90): Empty array "pop" detected here. diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_loop_safe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_loop_safe.sol new file mode 100644 index 000000000..25986da7b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/pop_loop_safe.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; + +contract C { + uint[] a; + function f(uint l) public { + for (uint i = 0; i < l; ++i) { + a.push(); + a.pop(); + } + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol new file mode 100644 index 000000000..5d4241984 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C { + uint[] a; + function f(uint l) public { + for (uint i = 0; i < l; ++i) { + a.push(); + a.pop(); + } + a.pop(); + } +} +// ---- +// Warning: (150-157): Empty array "pop" detected here. diff --git a/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_safe.sol b/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_safe.sol new file mode 100644 index 000000000..34a1ae680 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_safe.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C { + uint[][] a; + function f(uint[] memory x, uint y) public { + a.push(x); + a[0].push(y); + assert(a[0][a[0].length - 1] == y); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol new file mode 100644 index 000000000..d5bd19bb1 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C { + uint[][] a; + function f(uint[] memory x, uint y) public { + a.push(x); + a[0].push(y); + a[0].pop(); + assert(a[0][a[0].length - 1] == y); + } +} +// ---- +// Warning: (162-177): Underflow (resulting value less than 0) happens here +// Warning: (150-184): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/array_members/push_arg_1.sol b/test/libsolidity/smtCheckerTests/array_members/push_arg_1.sol new file mode 100644 index 000000000..e36895554 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/push_arg_1.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; + +contract C { + uint[] a; + function f(uint x) public { + a.push(x); + assert(a[a.length - 1] == x); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol b/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol new file mode 100644 index 000000000..f563504f4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C { + uint256[] x; + constructor() public { x.push(42); } + function f() public { + x.push(23); + assert(x[0] == 42 || x[0] == 23); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe_no_overflow_assumption.sol b/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe_no_overflow_assumption.sol new file mode 100644 index 000000000..7ed99a69e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe_no_overflow_assumption.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C { + uint256[] x; + constructor() public { x.push(42); } + function f() public { + x.push(23); + assert(x[0] == 42); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe.sol b/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe.sol new file mode 100644 index 000000000..340f670d0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe.sol @@ -0,0 +1,12 @@ +contract C { + uint256[] x; + function f(uint256 l) public { + require(x.length == 0); + x.push(42); + x.push(84); + for(uint256 i = 0; i < l; ++i) + x.push(23); + assert(x[0] == 42 || x[0] == 23); + } +} + diff --git a/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol b/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol new file mode 100644 index 000000000..1f468f592 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + uint256[] x; + function f(uint256 l) public { + require(x.length == 0); + x.push(42); + x.push(84); + for(uint256 i = 0; i < l; ++i) + x.push(23); + assert(x[0] == 42); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol new file mode 100644 index 000000000..8ad5cdcad --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C { + uint[][] a; + function f() public { + a.push(); + uint[] storage b = a[0]; + b.push(8); + assert(b[b.length - 1] == 8); + // Safe but fails due to aliasing. + assert(a[0][a[0].length - 1] == 8); + } +} +// ---- +// Warning: (217-232): Underflow (resulting value less than 0) happens here +// Warning: (205-239): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol new file mode 100644 index 000000000..f54fc8d83 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; + +contract C { + uint[][] a; + function f() public { + a.push(); + a[0].push(); + a[0][0] = 16; + uint[] storage b = a[0]; + b[0] = 32; + assert(a[0][0] == 16); + } +} +// ---- +// Warning: (167-188): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/array_members/push_zero_2d_safe.sol b/test/libsolidity/smtCheckerTests/array_members/push_zero_2d_safe.sol new file mode 100644 index 000000000..45a56e677 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/push_zero_2d_safe.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C { + uint[][] a; + function f() public { + a.push(); + a[0].push(); + assert(a[a.length - 1][0] == 0); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol new file mode 100644 index 000000000..9b9516ccd --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; + +contract C { + uint[][] a; + function f() public { + a.push(); + a[0].push(); + assert(a[a.length - 1][0] == 100); + } +} +// ---- +// Warning: (111-144): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/array_members/push_zero_safe.sol b/test/libsolidity/smtCheckerTests/array_members/push_zero_safe.sol new file mode 100644 index 000000000..e8054e361 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/push_zero_safe.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; + +contract C { + uint[] a; + function f() public { + a.push(); + assert(a[a.length - 1] == 0); + } +} diff --git a/test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol new file mode 100644 index 000000000..966b4e1bd --- /dev/null +++ b/test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; + +contract C { + uint[] a; + function f() public { + a.push(); + assert(a[a.length - 1] == 100); + } +} +// ---- +// Warning: (94-124): Assertion violation happens here